Inference at * 2 1 1 1 2 1 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
6. i : 
7. i < ||l1||
  l1[i] = l2[(i+(||l2|| - ||l1||))] 

latex

 by ((InstHyp [i] (-3)) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 8. l1[i] = l2[((||l2|| - ||l1||)+i)]
C1:   l1[i] = l2[(i+(||l2|| - ||l1||))]
C.

Definitions

t  T, l[i], n+m, n - m, a < b, x:A. B(x), x:AB(x), type List, Type, , {x:A| B(x)} , , A  B, A, False, P  Q, s = t, ||as||